Nuprl Definition : d-world
11,40
postcript
pdf
d-world(
D
;
v
;
sched
;
dec
;
discrete
)
== <
i
,
x
. M(
i
).ds(
x
)
==
,
i
,
a
. M(
i
).da(locl(
a
))
==
,
l
,
tg
. M(source(
l
)).dout(
l
,
tg
)
==
,
i
,
t
. if (
t
=
0)
==
then
x
.M(
i
).init(
x
)?
v
(
i
,
x
)
==
else (CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))((
t
- 1),
i
)).1
==
fi
==
,
i
,
t
. ((CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))(
t
,
i
)).2).1
==
,
i
,
t
. (CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))(
t
,
i
)).2.2
==
,
i
.d-machine(
i
;M(
i
);
dec
(
i
))
==
,
discrete
==
,
>
latex
clarification:
d-world{i:l}
d-world
(
D
;
v
;
sched
;
dec
;
discrete
)
== <
i
,
x
. d-m(
D
;
i
).ds(
x
)
==
,
i
,
a
. d-m(
D
;
i
).da(locl(
a
))
==
,
l
,
tg
. d-m(
D
; source(
l
)).dout(
l
,
tg
)
==
,
i
,
t
. if (
t
=
0)
==
then
x
.d-m(
D
;
i
).init(
x
)?
v
(
i
,
x
)
==
else (CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))((
t
- 1),
i
)).1
==
fi
==
,
i
,
t
. ((CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))(
t
,
i
)).2).1
==
,
i
,
t
. (CV(d-comp(
D
;
v
;
sched
;
dec
;
discrete
))(
t
,
i
)).2.2
==
,
i
.d-machine(
i
;d-m(
D
;
i
);
dec
(
i
))
==
,
discrete
==
,
>
latex
Definitions
M
.ds(
x
)
,
M
.da(
a
)
,
locl(
a
)
,
M
.dout(
l
,
tg
)
,
source(
l
)
,
if
b
then
t
else
f
fi
,
(
i
=
j
)
,
M
.init(
x
)?
v
,
n
-
m
,
#$n
,
t
.1
,
t
.2
,
CV(
F
)
,
d-comp(
D
;
v
;
sched
;
dec
;
d
)
,
x
.
A
(
x
)
,
d-machine(
i
;
M
;
dec
)
,
M(
i
)
,
f
(
a
)
,
<
a
,
b
>
,
FDL editor aliases
d-world
origin